n, m:, f, g:(nm).
(x:n, y:m. f(x,y) = g(x,y))  sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)   

latex

Definitions	sum(f(x;y) | x < n; y < m), sum(f(x) | x < k), x. t(x), t  T, {i..j}, , i  j < k, AB, P & Q, A, False, P  Q, x(s1,s2), x:A. B(x)
Lemmas	sum functionality, sum wf, int seg wf, nat wf